T:Type, as2, bs2, as1, bs1:T List.
as1  as2  bs1  bs2  agree_on_common(T;as2;bs2)  agree_on_common(T;as1;bs1) 

latex

Definitions	t  T, x:A. B(x), agree_on_common(T;as;bs), l1  l2, P  Q, P & Q, P  Q, b, True, P  Q, {T}, SQType(T), Prop, (x  l), A, P  Q, False
Lemmas	cons member, iseg member, not wf, l member wf, implies functionality wrt iff, cons iseg, agree on common nil, iseg nil, assert of null, iseg wf, agree on common wf